*****∧i REPL[A←λx t.(∀y.(yεt ≡ yεa ∧ R(x,y)))];

1 ∀x.∃y.∀z.(∀y.(yεz≡(yεa∧R(x,y)))≡y=z)⊃∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(s,y)))))  

*****∧i SEP[B←λy.R(x,y)];

2 ∀x1.∃y.∀z.(zεy≡(zεx1∧R(x,z)))  

*****∀E ↑ a;

3 ∃y.∀z.(zεy≡(zεa∧R(x,z)))  

*****∃E ↑ w;

4 ∀z.(zεw≡(zεa∧R(x,z)))  (4)

*****ASSUME ∀z.(zεt≡(zεa∧R(x,z)));

5 ∀z.(zεt≡(zεa∧R(x,z)))  (5)

*****∀E EXT w,t;

6 ∀z.(zεw≡zεt)≡w=t  

*****∀E ↑↑↑ z;

7 zεw≡(zεa∧R(x,z))  (4)

*****∀E ↑↑↑ z;

8 zεt≡(zεa∧R(x,z))  (5)

*****TAUT zεw≡zεt 7:8;

9 zεw≡zεt  (4 5)

*****∀I ↑ z;

10 ∀z.(zεw≡zεt)  (4 5)

*****TAUT w=t 6,10;

11 w=t  (4 5)

*****⊃I 5⊃↑;

12 ∀z.(zεt≡(zεa∧R(x,z)))⊃w=t  (4)

*****ASSUME w=t;

13 w=t  (13)

*****SUBST ↑ IN 4;

14 ∀z.(zεt≡(zεa∧R(x,z)))  (4 13)

*****⊃I ↑↑⊃↑;

15 w=t⊃∀z.(zεt≡(zεa∧R(x,z)))  (4)

*****TAUT ∀z.(zεt≡(zεa∧R(x,z)))≡w=t 12,15;

16 ∀z.(zεt≡(zεa∧R(x,z)))≡w=t  (4)

*****∀I ↑ t;

17 ∀t.(∀z.(zεt≡(zεa∧R(x,z)))≡w=t)  (4)

*****∃I ↑ w←y;

18 ∃y.∀t.(∀z.(zεt≡(zεa∧R(x,z)))≡y=t)  

*****∀I ↑ x;

19 ∀x.∃y.∀t.(∀z.(zεt≡(zεa∧R(x,z)))≡y=t)  

*****TAUT ∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(s,y))))) 1,19;

20 ∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(s,y)))))  

*****∀E ↑ a;

21 ∃v.∀r.(rεv≡∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))))  

*****∃E ↑ v;

22 ∀r.(rεv≡∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))))  (22)

*****∀E UNION v;

23 ∀z.(zεunion v≡∃t.(tεv∧zεt))  

*****∀E ↑ z;

24 zεunion v≡∃t.(tεv∧zεt)  

*****ASSUME zεunion v;

25 zεunion v  (25)

*****TAUT ∃t.(tεv∧zεt) 24:25;

26 ∃t.(tεv∧zεt)  (25)

*****∃E ↑ t;

27 tεv∧zεt  (27)

*****∀E 22 t;

28 tεv≡∃s.(sεa∧∀y.(yεt≡(yεa∧R(s,y))))  (22)

*****TAUT ∃s.(sεa∧∀y.(yεt≡(yεa∧R(s,y)))) 27:28;

29 ∃s.(sεa∧∀y.(yεt≡(yεa∧R(s,y))))  (22 27)

*****∃E ↑ s;

30 sεa∧∀y.(yεt≡(yεa∧R(s,y)))  (30)

*****∧E ↑:#2;

31 ∀y.(yεt≡(yεa∧R(s,y)))  (30)

*****∀E ↑ z;

32 zεt≡(zεa∧R(s,z))  (30)

*****TAUT zεa 27,32;

33 zεa  (22 25)

*****⊃I 25⊃↑;

34 zεunion v⊃zεa  (22)

*****ASSUME zεa;

35 zεa  (35)

*****∧I SEP[B←λy.R(z,y)];

36 ∀x.∃y.∀z1.(z1εy≡(z1εx∧R(z,z1)))  

*****∀E ↑ a;

37 ∃y.∀z1.(z1εy≡(z1εa∧R(z,z1)))  

*****∃E ↑ y;

38 ∀z1.(z1εy≡(z1εa∧R(z,z1)))  (38)

*****∧I ((35 38));

39 zεa∧∀z1.(z1εy≡(z1εa∧R(z,z1)))  (35 38)

*****∃I ↑ z←s;

40 ∃s.(sεa∧∀z1.(z1εy≡(z1εa∧R(s,z1))))  (35 38)

*****∀E 22 y;

41 yεv≡∃s.(sεa∧∀y1.(y1εy≡(y1εa∧R(s,y1))))  (22)

*****TAUT yεv 40:41;

42 yεv  (22 35 38)

*****∀E 38 z;

43 zεy≡(zεa∧R(z,z))  (38)

*****∀E EQUIV1 z;

44 R(z,z)  

*****TAUT zεy 35,43:44;

45 zεy  (35 38)

*****∧I ((42 45));

46 yεv∧zεy  (22 35 38)

*****∃I ↑ y←t;

47 ∃t.(tεv∧zεt)  (22 35)

*****TAUT zεunion v 24,47;

48 zεunion v  (22 35)

*****⊃I 35⊃↑;

49 zεa⊃zεunion v  (22)

*****TAUT zεunion v≡zεa 34,49;

50 zεunion v≡zεa  (22)

*****∀I ↑ z;

51 ∀z.(zεunion v≡zεa)  (22)

*****∀E EXT union v,a;

52 ∀z.(zεunion v≡zεa)≡union v=a  

*****TAUT union v=a 51:52;

53 union v=a  (22)

*****ASSUME rεv;

54 rεv  (54)

*****∀E 22 r;

55 rεv≡∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y))))  (22)

*****TAUT ∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))) 54:55;

56 ∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y))))  (22 54)

*****ASSUME xεr∧yεr;

57 xεr∧yεr  (57)

*****∃E ↑↑ s;

58 sεa∧∀y.(yεr≡(yεa∧R(s,y)))  (58)

*****∧E ↑:#2;

59 ∀y.(yεr≡(yεa∧R(s,y)))  (58)

*****∀E ↑ x;

60 xεr≡(xεa∧R(s,x))  (58)

*****∀E ↑↑ y;

61 yεr≡(yεa∧R(s,y))  (58)

*****∀E EQUIV2 s,x;

62 R(s,x)≡R(x,s)  

*****∀E EQUIV3 x,s,y;

63 (R(x,s)∧R(s,y))⊃R(x,y)  

*****TAUT R(x,y) 57,60:63;

64 R(x,y)  (22 54 57)

*****⊃I 57⊃↑;

65 (xεr∧yεr)⊃R(x,y)  (22 54)

*****∀I ↑ x y;

66 ∀x y.((xεr∧yεr)⊃R(x,y))  (22 54)

*****⊃I 54⊃↑;

67 rεv⊃∀x y.((xεr∧yεr)⊃R(x,y))  (22)

*****∀I ↑ r;

68 ∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))  (22)

*****ASSUME r1εv∧r2εv;

69 r1εv∧r2εv  (69)

*****ASSUME ∃x.(xεr1∧xεr2);

70 ∃x.(xεr1∧xεr2)  (70)

*****∀E 22 r1;

71 r1εv≡∃s.(sεa∧∀y.(yεr1≡(yεa∧R(s,y))))  (22)

*****∀E 22 r2;

72 r2εv≡∃s.(sεa∧∀y.(yεr2≡(yεa∧R(s,y))))  (22)

*****TAUT ∃s.(sεa∧∀y.(yεr1≡(yεa∧R(s,y)))) 69,71;

73 ∃s.(sεa∧∀y.(yεr1≡(yεa∧R(s,y))))  (22 69)

*****TAUT ∃s.(sεa∧∀y.(yεr2≡(yεa∧R(s,y)))) 69,72;

74 ∃s.(sεa∧∀y.(yεr2≡(yεa∧R(s,y))))  (22 69)

*****∃E ↑↑ s;

75 sεa∧∀y.(yεr1≡(yεa∧R(s,y)))  (75)

*****∃E ↑↑ t;

76 tεa∧∀y.(yεr2≡(yεa∧R(t,y)))  (76)

*****∧E ↑↑:#2;

77 ∀y.(yεr1≡(yεa∧R(s,y)))  (75)

*****∧E ↑↑:#2;

78 ∀y.(yεr2≡(yεa∧R(t,y)))  (76)

*****∀E ↑↑ x;

79 xεr1≡(xεa∧R(s,x))  (75)

*****∀E ↑↑ x;

80 xεr2≡(xεa∧R(t,x))  (76)

*****∀E 77 w;

81 wεr1≡(wεa∧R(s,w))  (75)

*****∀E 78 w;

82 wεr2≡(wεa∧R(t,w))  (76)

*****LABEL A;

*****∃E 70 x;

83 xεr1∧xεr2  (83)

*****∀E EQUIV2 s,w;

84 R(s,w)≡R(w,s)  

*****∀E EQUIV2 x,t;

85 R(x,t)≡R(t,x)  

*****∀E EQUIV2 w,t;

86 R(w,t)≡R(t,w)  

*****∀E EQUIV2 x,s;

87 R(x,s)≡R(s,x)  

*****∀E EQUIV3 w,s,x;

88 (R(w,s)∧R(s,x))⊃R(w,x)  

*****∀E EQUIV3 w,x,t;

89 (R(w,x)∧R(x,t))⊃R(w,t)  

*****∀E EQUIV3 w,t,x;

90 (R(w,t)∧R(t,x))⊃R(w,x)  

*****LABEL B;

*****∀E EQUIV3 w,x,s;

91 (R(w,x)∧R(x,s))⊃R(w,s)  

*****TAUT wεr1≡wεr2 79:B;

92 wεr1≡wεr2  (22 69 70)

*****∀I ↑ w;

93 ∀w.(wεr1≡wεr2)  (22 69 70)

*****∀E EXT r1,r2;

94 ∀z.(zεr1≡zεr2)≡r1=r2  

*****TAUT r1=r2 93:94;

95 r1=r2  (22 69 70)

*****⊃I 70⊃↑;

96 ∃x.(xεr1∧xεr2)⊃r1=r2  (22 69)

*****⊃I 69⊃↑;

97 (r1εv∧r2εv)⊃(∃x.(xεr1∧xεr2)⊃r1=r2)  (22)

*****TAUT ((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2 97;

98 ((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2  (22)

*****∀I ↑ r1 r2;

99 ∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2)  (22)

*****TAUT union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2)) 53,68,99;

100 union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2))  (22)

*****∃I ↑ v ;

101 ∃v.(union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2)))  

*****∀I ↑ a;

102 ∀a.∃v.(union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2)))